(declare-const Str2 String)
(declare-const Str3 String)
(declare-const Str17 String)
(assert (= false false false false false false false (= Str17 Str2 Str3) false false))
(check-sat)
(declare-const Str2 String)
(declare-const Str18 String)
(assert (distinct Str18 Str2))
(check-sat)
